(DEFUN NORMALIZE (E) 
       (IF (OR (ISVAR E) (ATOM E))
	   E
	   (ISLAM E)
	   (MKLAM (FPAR E) (NORMALIZE (BODY E)))
	   (ISVAR (FUN E))
	   (MKAP (FUN E) (NORMALIZELIST (APAR E)))
	   (ATOM (FUN E))
	   (NORMALIZE (MKAP (VAL (FUN E)) (APAR E)))
	   (ISLAM (FUN E))
	   (NORMALIZE (CONVERT E))
	   ;;;	   (NORMALIZE (IF (NULL (FPAR (FUN E)))
	   ;;;			  (BODY (FUN E))
	   ;;;			  (NULL (APAR E))
	   ;;;			  (FUN E)
	   ;;;			  (MKAP (SUBLAM (CAR (APAR E))
	   ;;;					(CAR (FPAR (FUN E)))
	   ;;;					(MKLAM (CDR (FPAR (FUN
	   E)) 

;;;					       (BODY (FUN E)))
;;;				(CDR (APAR E)))))

(NOT (NORMAL (FUN E))) 

(NORMALIZE (MKAP (CONVERT (FUN E)) (APAR E))) 

(MKAP (FUN E) (NORMALIZELIST (APAR E))) 

(DEFUN STEP1 (N) 
       (PROG (M) 
	     (SETQ M 0.)
	LOOP (COND ((OR (= M N) (EQUAL Z (SETQ Z (CONVERT Z))))
		    (RETURN (LIST M Z))))
	     (SETQ M (ADD1 M))
	     (GO LOOP))) 

(DEFUN NORMALIZE2 (E) 
       (PROG (W) 
	     (SETQ W E)
	LOOP (IF (EQUAL W (SETQ W (CONVERT W)))
		 (RETURN W)
		 (GO LOOP)))) 

;;; (normal e) means that e is in normal form.

(DEFUN NORMAL (E) 
       (OR (ISVAR E)
	   (AND (ISLAM E) (NORMAL (BODY E)))
	   (AND (OR (ISVAR (FUN E))
		    (AND (ATOM (FUN E))
			 (NORMAL (MKAP (VAL (FUN E)) (APAR E))))
		    (AND (NOT (ATOM (FUN E))) (NOT (ISLAM (FUN E)))))
		(NORMLIS (APAR E))))) 

(DEFUN NORMLIS (U) 
       (OR (NULL U) (AND (NORMAL (CAR U)) (NORMLIS (CDR U))))) 

;;; Normalizing a λ-calculus expression.  Avoiding the capture of free
;;; variables is the cause of most of the complications.

(DEFUN NORMALIZE (E) 
       (IF (OR (ISVAR E) (ATOM E))
	   E
	   (ISLAM E)
	   (MKLAM (FPAR E) (NORMALIZE (BODY E)))
	   (ISVAR (FUN E))
	   (MKAP (FUN E) (NORMALIZELIST (APAR E)))
	   (ATOM (FUN E))
	   (NORMALIZE (MKAP (VAL (FUN E)) (APAR E)))
	   (ISLAM (FUN E))
	   (NORMALIZE (IF (NULL (FPAR (FUN E)))
			  (BODY (FUN E))
			  (NULL (APAR E))
			  (FUN E)
			  (MKAP (SUBLAM (CAR (APAR E))
					(CAR (FPAR (FUN E)))
					(MKLAM (CDR (FPAR (FUN E)))
					       (BODY (FUN E))))
				(CDR (APAR E)))))
	   (NOT (NORMAL (FUN E)))
	   (NORMALIZE (MKAP (NORMALIZE (FUN E)) (APAR E)))
	   (MKAP (FUN E) (NORMALIZELIST (APAR E))))) 

(DEFUN NORMALIZELIST (U) 
       (IF (NULL U)
	   NIL
	   (CONS (NORMALIZE (CAR U)) (NORMALIZELIST (CDR U)))))